skip to main content

Explore Research Products in the NSF-PAR

  • Home
  • Search Results
  • Page 1 of 1

Search for: All records

Editors contains: "Hyvarinen, Antti E."

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. ; ; ( , Satisfiability Modulo Theories workshop, CEUR Workshop Proceedings)
    Deharbe, David ; Hyvarinen, Antti E. (Ed.)
    CDSAT (Conflict-Driven Satisfiability) is a paradigm for theory combination that works by coordinating theory modules to reason in the union of the theories in a conflict-driven manner. We generalize CDSAT to the case of nondisjoint theories by presenting a new CDSAT theory module for a theory of arrays with abstract length, which is an abstraction of the theory of arrays with length. The length function is a bridging function as it forces theories to share symbols, but the proposed abstraction limits the sharing to one predicate symbol. The CDSAT framework handles shared predicates with minimal changes, and the new module satisfies the CDSAT requirements, so that completeness is preserved. 
    more » « less
    Accepted Manuscript Full Text Available